package kodkod.analysis.visitor;

import kodkod.ast.BinaryExpression;
import kodkod.ast.BinaryFormula;
import kodkod.ast.BinaryIntExpression;
import kodkod.ast.ComparisonFormula;
import kodkod.ast.Comprehension;
import kodkod.ast.ConstantExpression;
import kodkod.ast.ConstantFormula;
import kodkod.ast.Decl;
import kodkod.ast.Decls;
import kodkod.ast.ExprToIntCast;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.IfExpression;
import kodkod.ast.IfIntExpression;
import kodkod.ast.IntComparisonFormula;
import kodkod.ast.IntConstant;
import kodkod.ast.IntExpression;
import kodkod.ast.IntToExprCast;
import kodkod.ast.LeafExpression;
import kodkod.ast.MultiplicityFormula;
import kodkod.ast.NaryExpression;
import kodkod.ast.NaryFormula;
import kodkod.ast.NaryIntExpression;
import kodkod.ast.Node;
import kodkod.ast.NotFormula;
import kodkod.ast.ProjectExpression;
import kodkod.ast.QuantifiedFormula;
import kodkod.ast.Relation;
import kodkod.ast.RelationPredicate;
import kodkod.ast.SumExpression;
import kodkod.ast.UnaryExpression;
import kodkod.ast.UnaryIntExpression;
import kodkod.ast.Variable;
import kodkod.ast.visitor.VoidVisitor;

public abstract class AbstractAnalyzer implements VoidVisitor {
	
	abstract void beginChild(Node parent, Node child);
	abstract boolean visited(Node node);
	abstract void foundLeafExpression(LeafExpression leaf);
	abstract void endChild(Node parent, Node child);
		
	/**
	 * Visits all the children of the given declarations node if
	 * this.visited(decls) returns false.  Otherwise does nothing.
	 * @effects all d: declarations.declarations | d.variable.accept(this) && d.expression.accept(this)
	 */
	public void visit(Decls decls) {
		if (visited(decls)) return;
		for (Decl decl : decls) {
			beginChild(decls, decl);
			decl.accept(this);
			endChild(decls, decl);
		}
	}
	
	/**
	 * Visits the variable and expression of this decl if
	 * this.visited(decl) returns false.  Otherwise does nothing.
	 * @effects decl.variable.accept(this) && decl.expression.accept(this)
	 */
	public void visit(Decl decl) {
		if (visited(decl)) return;
		
		beginChild(decl, decl.variable());
		decl.variable().accept(this);
		endChild(decl, decl.variable());
		
		beginChild(decl, decl.expression());
		decl.expression().accept(this);
		endChild(decl, decl.expression());
		
		beginChild(decl.expression(), decl.variable());
		endChild(decl.expression(), decl.variable());
	}
	
	public void visit(Relation relation) {
		foundLeafExpression(relation);
	}
	public void visit(Variable variable) {
		foundLeafExpression(variable);
	}
	public void visit(ConstantExpression constExpr) {
		foundLeafExpression(constExpr);
	}
	
	/**
	 * Visits the children if this.visited(expr) returns false.  Otherwise does nothing.
	 * @effects all i: [0..#expr.children) | expr.child(i).accept(this)
	 */
	public void visit(NaryExpression expr) {
		if (visited(expr)) return;
		for(Expression child : expr) { 
			beginChild(expr, child);
			child.accept(this);
			endChild(expr, child);
		}
	}
	
	/**
	 * Visits the left and right subexpressions  if
	 * this.visited(binExpr) returns false.  Otherwise does nothing.
	 * @effects binExpr.left.accept(this) && binExpr.right.accept(this)
	 */
	public void visit(BinaryExpression binExpr) {
		if (visited(binExpr)) return;
		beginChild(binExpr, binExpr.left());
		binExpr.left().accept(this);
		endChild(binExpr, binExpr.left());
		
		beginChild(binExpr, binExpr.right());
		binExpr.right().accept(this);
		endChild(binExpr, binExpr.right());
	}
	
	/**
	 * Visits the subexpression  if
	 * this.visited(unaryExpr) returns false.  Otherwise does nothing.
	 * @effects unaryExpr.expression.accept(this)
	 */
	public void visit(UnaryExpression unaryExpr) {
		if (visited(unaryExpr)) return;
		beginChild(unaryExpr, unaryExpr.expression());
		unaryExpr.expression().accept(this);
		endChild(unaryExpr, unaryExpr.expression());
	}
	
	/**
	 * Visits the declarations and the formula  if
	 * this.visited(comprehension) returns false.  Otherwise does nothing.
	 * @effects comprehension.declarations.accept(this) && comprehension.formula.accept(this)
	 */
	public void visit(Comprehension comprehension) {
		if (visited(comprehension)) return;
		beginChild(comprehension, comprehension.decls());
		comprehension.decls().accept(this);
		endChild(comprehension, comprehension.decls());
		
		beginChild(comprehension, comprehension.formula());
		comprehension.formula().accept(this);
		endChild(comprehension, comprehension.formula());
	}
	
	/**
	 * Visits the if-condition, the then-expression, and the else-expression  if
	 * this.visited(ifExpr) returns false.  Otherwise does nothing.
	 * @effects ifExpr.condition.accept(this) && ifExpr.thenExpr.accept(this) &&
	 *          ifExpr.elseExpr.accept(this)
	 */
	public void visit(IfExpression ifExpr) {
		if (visited(ifExpr)) return;
		beginChild(ifExpr, ifExpr.condition());
		ifExpr.condition().accept(this);
		endChild(ifExpr, ifExpr.condition());
		
		beginChild(ifExpr, ifExpr.thenExpr());
		ifExpr.thenExpr().accept(this);
		endChild(ifExpr, ifExpr.thenExpr());
		
		beginChild(ifExpr, ifExpr.elseExpr());
		ifExpr.elseExpr().accept(this);
		endChild(ifExpr, ifExpr.elseExpr());
	}
	
	/**
	 * Visits project.expression and project.columns if this.visited(project) returns false.
	 * Otherwise does nothing.
	 * @effects project.expression.accept(this) && all i: project.arity | project.columns[i].accept(this)
	 */
	public void visit(ProjectExpression project) {
		if (visited(project)) return;
		beginChild(project, project.expression());
		project.expression().accept(this);
		endChild(project, project.expression());
		
		for(int i = 0, arity = project.arity(); i < arity; i++) {
			beginChild(project, project.column(i));
			project.column(i).accept(this);
			endChild(project, project.column(i));
		}
	}
	
	/**
	 * Visits castExpr.intExpr  if
	 * this.visited(castExpr) returns false.  Otherwise does nothing.
	 * @effects castExpr.expression.accept(this)
	 */
	public void visit(IntToExprCast castExpr) {
		if (visited(castExpr)) return;
		beginChild(castExpr, castExpr.intExpr());
		castExpr.intExpr().accept(this);
		endChild(castExpr, castExpr.intExpr());
	}

	/**
	 * Does nothing.
	 */
	public void visit(IntConstant intConst) {}
	
	/**
	 * Visits the if-condition, the then-expression, and the else-expression  if
	 * this.visited(intExpr) returns false.  Otherwise does nothing.
	 * @effects intExpr.condition.accept(this) && intExpr.thenExpr.accept(this) &&
	 *          intExpr.elseExpr.accept(this)
	 */
	public void visit(IfIntExpression intExpr) {
		if (visited(intExpr)) return;
		beginChild(intExpr, intExpr.condition());
		intExpr.condition().accept(this);
		endChild(intExpr, intExpr.condition());
		
		beginChild(intExpr, intExpr.thenExpr());
		intExpr.thenExpr().accept(this);
		endChild(intExpr, intExpr.thenExpr());

		beginChild(intExpr, intExpr.elseExpr());
		intExpr.elseExpr().accept(this);
		endChild(intExpr, intExpr.elseExpr());
	}
	
	/**
	 * Visits intExpr.expression  if
	 * this.visited(intExpr) returns false.  Otherwise does nothing.
	 * @effects intExpr.expression.accept(this)
	 */
	public void visit(ExprToIntCast intExpr) {
		if (visited(intExpr)) return;
		beginChild(intExpr, intExpr.expression());
		intExpr.expression().accept(this);
		endChild(intExpr, intExpr.expression());
	}
	
	/**
	 * Visits the children if this.visited(intExpr) returns false.  Otherwise does nothing.
	 * @effects all i: [0..#intExpr.children) | intExpr.child(i).accept(this)
	 */
	public void visit(NaryIntExpression intExpr) {
		if (visited(intExpr)) return;
		for(IntExpression child : intExpr) { 
			beginChild(intExpr, child);
			child.accept(this);
			endChild(intExpr, child);
		}
	}
	
	/**
	 * Visits the children of the given integer expression  if
	 * this.visited(intExpr) returns false.  Otherwise does nothing.
	 * @effects intExpr.left.accept(this) && intExpr.right.accept(this)
	 */
	public void visit(BinaryIntExpression intExpr) {
		if (visited(intExpr)) return;
		beginChild(intExpr, intExpr.left());
		intExpr.left().accept(this);
		endChild(intExpr, intExpr.left());
		
		beginChild(intExpr, intExpr.right());
		intExpr.right().accept(this);
		endChild(intExpr, intExpr.right());
	}
	
	/**
	 * Visits the subexpression  if
	 * this.visited(intExpr) returns false.  Otherwise does nothing.
	 * @effects unaryExpr.expression.accept(this)
	 */
	public void visit(UnaryIntExpression intExpr) {
		if (visited(intExpr)) return;
		beginChild(intExpr, intExpr.intExpr());
		intExpr.intExpr().accept(this);
		endChild(intExpr, intExpr.intExpr());
	}
	
	/**
	 * Visits the children of the given sum expression  if
	 * this.visited(intExpr) returns false.  Otherwise does nothing.
	 * @effects intExpr.decls.accept(this) && intExpr.intExpr.accept(this)
	 */
	public void visit(SumExpression intExpr) {
		if (visited(intExpr)) return;
		beginChild(intExpr, intExpr.decls());
		intExpr.decls().accept(this);
		endChild(intExpr, intExpr.decls());
		
		beginChild(intExpr, intExpr.intExpr());
		intExpr.intExpr().accept(this);
		endChild(intExpr, intExpr.intExpr());
	}
	
	/**
	 * Visits the children of the given integer comparison formula  if
	 * this.visited(intComp) returns false.  Otherwise does nothing.
	 * @effects intComp.left.accept(this) && intComp.right.accept(this)
	 */
	public void visit(IntComparisonFormula intComp) {
		if (visited(intComp)) return;
		beginChild(intComp, intComp.left());
		intComp.left().accept(this);
		endChild(intComp, intComp.left());

		beginChild(intComp, intComp.right());
		intComp.right().accept(this);
		endChild(intComp, intComp.right());
	}
	
	/**
	 * Visits the declarations and the formula  if
	 * this.visited(quantFormula) returns false.  Otherwise does nothing.
	 * @effects quantFormula.declarations.accept(this) && quantFormula.formula.accept(this)
	 */
	public void visit(QuantifiedFormula quantFormula) {
		if (visited(quantFormula)) return;
		beginChild(quantFormula, quantFormula.decls());
		quantFormula.decls().accept(this);
		endChild(quantFormula, quantFormula.decls());
		
		beginChild(quantFormula, quantFormula.formula());
		quantFormula.formula().accept(this);
		endChild(quantFormula, quantFormula.formula());
	}
	
	/**
	 * Visits the children if this.visited(formula) returns false.  Otherwise does nothing.
	 * @effects all i: [0..#formula.children) | formula.child(i).accept(this)
	 */
	public void visit(NaryFormula formula) {
		if (visited(formula)) return;
		for(Formula child : formula) { 
			if (child instanceof ComparisonFormula) { 
				// escape self-equalities
				ComparisonFormula cf = (ComparisonFormula)child;
				if (cf.left() == cf.right()) continue;
			}
			beginChild(formula, child);
			child.accept(this);
			endChild(formula, child);
		}
	}
	
	/**
	 * Visits the left and right children  if
	 * this.visited(binFormula) returns false.  Otherwise does nothing.
	 * @effects binFormula.left.accept(this) && binFormula.right.accept(this)
	 */
	public void visit(BinaryFormula binFormula) {
		if (visited(binFormula)) return;
		beginChild(binFormula, binFormula.left());
		binFormula.left().accept(this);
		endChild(binFormula, binFormula.left());
		
		beginChild(binFormula, binFormula.right());
		binFormula.right().accept(this);
		endChild(binFormula, binFormula.right());
	}
	
	/**
	 * Visits the subformula  if
	 * this.visited(not) returns false.  Otherwise does nothing.
	 * @effects not.formula.accept(this)
	 */
	public void visit(NotFormula not) {
		if (visited(not)) return;
		beginChild(not, not.formula());
		not.formula().accept(this);
		endChild(not, not.formula());
	}
	
	/**
	 * Does nothing.
	 */
	public void visit(ConstantFormula constant) {}
	
	/**
	 * Visits the left and right children  if
	 * this.visited(compFormula) returns false.  Otherwise does nothing.
	 * @effects compFormula.left.accept(this) && compFormula.right.accept(this)
	 */
	public void visit(ComparisonFormula compFormula) {
		if (visited(compFormula)) return;
		beginChild(compFormula, compFormula.left());
		compFormula.left().accept(this);
		endChild(compFormula, compFormula.left());
		
		beginChild(compFormula, compFormula.right());
		compFormula.right().accept(this);
		endChild(compFormula, compFormula.right());
	}
	
	/**
	 * Visits the formula  if
	 * this.visited(multFormula) returns false.  Otherwise does nothing.
	 * @effects multFormula.expression.accept(this)
	 */
	public void visit(MultiplicityFormula multFormula) {
		if (visited(multFormula)) return;
		beginChild(multFormula, multFormula.expression());
		multFormula.expression().accept(this);
		endChild(multFormula, multFormula.expression());
	}
	
	/**
	 * Visits the children of the predicate  if
	 * this.visited(pred) returns false.  Otherwise does nothing.
	 * @effects pred.relation.accept(this) && 
	 *          (pred.name = FUNCTION => pred.domain.accept(this) && pred.range.accept(this)) && 
	 *          (pred.name = TOTAL_ORDERING => 
	 *            pred.ordered.accept(this) && pred.first.accept(this) && pred.last.accept(this) )
	 */
	public void visit(RelationPredicate pred) {
		if (visited(pred)) return;
		beginChild(pred, pred.relation());
		pred.relation().accept(this);
		endChild(pred, pred.relation());
		if (pred.name()==RelationPredicate.Name.FUNCTION) {
			final RelationPredicate.Function fp = (RelationPredicate.Function) pred;
			beginChild(pred, fp.domain());
			fp.domain().accept(this);
			endChild(pred, fp.domain());
			
			beginChild(pred, fp.range());
			fp.range().accept(this);
			endChild(pred, fp.range());
		} else if (pred.name()==RelationPredicate.Name.TOTAL_ORDERING) {
			final RelationPredicate.TotalOrdering tp = (RelationPredicate.TotalOrdering) pred;
			beginChild(pred, tp.ordered());
			tp.ordered().accept(this);
			endChild(pred, tp.ordered());
			
			beginChild(pred, tp.first());
			tp.first().accept(this);
			endChild(pred, tp.first());
			
			beginChild(pred, tp.last());
			tp.last().accept(this);
			endChild(pred, tp.last());
		}
	}
	
	public void visit(Node node) {
		if (node instanceof Decls) {
			if (node instanceof Decl) {
				visit((Decl)node);
			}
			visit((Decls)node);
		}
		if (node instanceof Expression) {
			if (node instanceof BinaryExpression) {
				visit((BinaryExpression)node);
			}
			if (node instanceof Comprehension) {
				visit((Comprehension)node);
			}
			if (node instanceof IfExpression) {
				visit((IfExpression)node);
			}
			if (node instanceof IntToExprCast) {
				visit((IntToExprCast)node);	
			}
			if (node instanceof LeafExpression) {
				if (node instanceof ConstantExpression) {
					visit((ConstantExpression)node);
				}	
				if (node instanceof Relation) {
					visit((Relation)node);
				}
				if (node instanceof Variable) {
					visit((Variable)node);
				}
			}
			if (node instanceof NaryExpression) {
				visit((NaryExpression)node);
			}
			if (node instanceof ProjectExpression) {
				visit((ProjectExpression)node);
			}
			if (node instanceof UnaryExpression) {
				visit((UnaryExpression)node);
			}
		}
		if (node instanceof Formula) {
			if (node instanceof BinaryFormula) {
				visit((BinaryFormula)node);
			}
			if (node instanceof ComparisonFormula) {
				visit((ComparisonFormula)node);
			}
			if (node instanceof ConstantFormula) {
				visit((ConstantFormula)node);
			}
			if (node instanceof IntComparisonFormula) {
				visit((IntComparisonFormula)node);
			}
			if (node instanceof MultiplicityFormula) {
				visit((MultiplicityFormula)node);
			}
			if (node instanceof NaryFormula) {
				visit((NaryFormula)node);
			}
			if (node instanceof NotFormula) {
				visit((NotFormula)node);
			}
			if (node instanceof QuantifiedFormula) {
				visit((QuantifiedFormula)node);
			}
			if (node instanceof RelationPredicate) {
				visit((RelationPredicate)node);
			}
		}
		if (node instanceof IntExpression) {
			if (node instanceof BinaryIntExpression) {
				visit((BinaryIntExpression)node);
			}
			if (node instanceof ExprToIntCast) {
				visit((ExprToIntCast)node);
			}
			if (node instanceof IfIntExpression) {
				visit((IfIntExpression)node);
			}
			if (node instanceof IntConstant) {
				visit((IntConstant)node);
			}
			if (node instanceof NaryIntExpression) {
				visit((NaryIntExpression)node);
			}
			if (node instanceof SumExpression) {
				visit((SumExpression)node);
			}
			if (node instanceof UnaryIntExpression) {
				visit((UnaryIntExpression)node);
			}
		}
	}
}
